The present invention relates to scaling logic verification, and more specifically, to simplifying a netlist by leveraging sequential unobservability conditions to eliminate gates by altering initial-value and next-state functions.
Contemporary hardware designs are typically complex and include a diversity of different logic such as bit-level control logic, data paths of various types (e.g., including pipeline stages, queues, and RAM) with error identification logic, performance related artifacts (e.g., pipelining, multi-threading, out-of-order execution, and power saving techniques), and pervasive logic artifacts used to initialize the design, monitor its runtime execution, and detect and cope with faults. While verifying hardware designs is necessary, the increased complexity of hardware designs has made verification more difficult.
Such designs are further complicated by the multi-dimensional optimization criteria including delay, area, and power—as well as the inclusion of logic to increase testability, reliability, and configurability. The verification of such complex systems has grown to be extremely challenging if not intractable, with verification resource demands having eclipsed the cost of all other aspects of the production of such systems, while nevertheless often entailing the risk of missed subtle design flaws. Such design flaws—especially in hardware—can be exorbitantly expensive to repair if exposed late, cause product delays, and risk serious damage due to erroneous computations.
Verification generally entails exponentially-growing complexity with respect to the size of the design under verification. Some verification techniques are more seriously hindered by certain design components than others. For example, techniques that leverage a canonical representation of design functionality may be more hindered by the number of primary inputs of the design than other size metrics—since a functional view (e.g., a truth table) is exponential in size with respect to the number of inputs. The number of gates of a design often imposes a significant impact on the complexity of analysis of the design functionality, since this often means that design function is often more complicated.
Techniques that reason about reachable states of a design are often highly impacted by the number of state elements of the design. Techniques which can reduce the size of the design under verification often make a tremendously positive impact on the tractability of the verification task. Such techniques can significantly reduce the expense of verification and thus production of a logic design, reducing the risk of missed bugs while enabling verification plan closure with less effort. Certain reduction techniques can furthermore be used in a synthesis setting, to reduce area and power of a logic circuit.